\lstset{numbers=none,
frame=none}

\section{Aclaraci\'on}
En nuestro caso, la funci\'on pertenece a la clase Telco. Sin embargo, no utiliza ni modifica los atributos privados de\\
Telco y por ende fueron omitidos trasnformaci\'on de estados.

\section{Especificaci\'on del problema}

\begin{problema}{infoGatewaysTE}{te: TelCO}{[(Gateway,\ent,\ent)]}
  \asegura[infoCorrecta]{mismos(result,\comp{(g,(\longitud{trivias(g)}, cuantosJueganAlgunaTrivia(te,g)))}{g \selec gateways(te)]})}
\end{problema}

\begin{aux}{cuantosJueganAlgunaTrivia}{t:TelCO,g:Gateway}{\ent}{
   \longitud{\comp{u}{u \selec usuarios(t),(\exists x \selec trivias(g))u \in participantes(x)}}}
\end{aux}

\section{Especificaci\'on de las funciones auxiliares}

\begin{problema}{usuariosDeLasTrivias}{this:TelCO, g:Gateway}{\ent}{
    \asegura{result == cuantosJueganAlgunaTrivia(this, ts)}}
\end{problema}

\begin{problema}{estaEnAlgunaTrivia}{this:TelCO, u:Usuario, ts:[Trivia]}{Bool}{
    \asegura{result == estaEnAlgunaTriviaAux(this, u, ts)}}
\end{problema}

\begin{aux}{estaEnAlgunaTriviaAux}{t:TelCO, u:Usuario, ts:[Trivia]}{Bool}{
    u \in (concat (\comp{participantes(ts_p)}{p \selec [0..\longitud{ts})})}
\end{aux}


\section{Transformaci\'on de estados del problema}

\subsection{Transformaci\'on de estados del cuerpo principal}

\begin{lstlisting}
Lista< pair<Gateway, pair< int,int > > > TelCO:: infoGateways() const{
  Lista< pair<Gateway, pair< int,int > > > lista;
\end{lstlisting}
$//E1: Vale\ lista == [] $ 
\begin{lstlisting}
  pair<Gateway, pair< int,int > > dupla;
\end{lstlisting}
$//E2: Vale\ lista == lista@E1 \ylogico dupla == (,)$ 
\begin{lstlisting}
  int i=0, cantTrivias=0, cantUsuarios=0;
\end{lstlisting}
$//E3: Vale\ lista == lista@E2 \ylogico dupla == dupla@E2 \ylogico \\
//i == cantTrivias == cantUsuarios == 0 \\
//Implica Pc: lista == [] \ylogico dupla == (,) \ylogico \\
//i == cantTrivias == cantUsuarios == 0$ 
\begin{lstlisting}
  while (i < gateways().longitud()){
\end{lstlisting}
$//Vale\ invariante\ I: 0 \leq i \leq \longitud{gateways(this)} \ylogico \\
//mismos (lista, \\
//\comp{(gateways(this)_j,(\longitud{trivias(gateways(this)_j)}, cuantosJueganAlgunaTrivia(this, gateways(this)_j)))}{j \selec [0..i)}) \\
//Funcion\ variante\ V: \longitud{gateways(this)} - i$
\begin{lstlisting}
    Gateway g = gateways().iesimo(i);
    cantTrivias = g.trivias().longitud();
    cantUsuarios = usuariosDeLasTrivias (g);
    dupla.first = g;
    dupla.second = pair <int,int> (cantTrivias,cantUsuarios);
    lista.agregar(dupla);
    i++;
  }
\end{lstlisting}
$//Qc: Vale\ mismos(lista, \comp{(gateways(this)_j,(\longitud{trivias(gateways(this)_j)},\\
//cuantosJueganAlgunaTrivia(this, gateways(this)_j)))}{j \selec [0..\longitud{gateways(this)})})$
\begin{lstlisting}
  return lista;
}
\end{lstlisting}

\subsection{Transformaci\'on de estados del cuerpo del ciclo}
\begin{lstlisting}
while (i < gateways().longitud()){
\end{lstlisting}
$//C1: Vale\ I \ylogico B$
\begin{lstlisting}
  Gateway g = gateways().iesimo(i);
\end{lstlisting}
$//C2: Vale\ g == gateways(this)_i \ylogico i == i@C1 \ylogico cantTrivias == cantTrivias@C1 \ylogico \\
//cantUsuarios == cantUsuarios@C1 \ylogico lista == lista@C1 \ylogico dupla == dupla@C1 $
\begin{lstlisting}
  cantTrivias = g.trivias().longitud();
\end{lstlisting}
$//C3: Vale\ g == g@C2 \ylogico i == i@C2 \ylogico cantTrivias == \longitud{trivias(g@C2)} \ylogico \\
//cantUsuarios == cantUsuarios@C2 \ylogico lista == lista@C2 \ylogico dupla == dupla@C2 $
\begin{lstlisting}
  cantUsuarios = usuariosDeLasTrivias (g);
\end{lstlisting}
$//C4: Vale\ g == g@C3 \ylogico i == i@C3 \ylogico cantTrivias == cantTrivias@C3 \ylogico \\
//cantUsuarios == cuantosJueganAlgunaTrivia(this, trivias(g)) \ylogico lista == lista@C3 \ylogico dupla == dupla@C3 $
\begin{lstlisting}
  dupla.first = g;
  dupla.second = pair <int,int> (cantTrivias,cantUsuarios);
\end{lstlisting}
$//C5: Vale\ g == g@C4 \ylogico i == i@C4 \ylogico cantTrivias == cantTrivias@C4 \ylogico \\
//cantUsuarios == cantUsuarios@C4 \ylogico lista == lista@C4 \ylogico \\
//dupla == (g@C4,(cantTrivias@C4,cantUsuarios@C4)) $
\begin{lstlisting}
  lista.agregar(dupla);
\end{lstlisting}
$//C6: Vale\ g == g@C5 \ylogico i == i@C5 \ylogico cantTrivias == cantTrivias@C5 \ylogico \\
//cantUsuarios == cantUsuarios@C5 \ylogico lista == dupla@C5 : lista@C5 \ylogico dupla == dupla@C5 $
Ac\'a usamos la especificaci\'on de agregar, sabiendo que los par\'ametros cumplen la precondici\'on.
\begin{lstlisting}
  i++;
\end{lstlisting}
$//C7: Vale\ g == g@C6 \ylogico i == i@C6 + 1 \ylogico cantTrivias == cantTrivias@C6 \ylogico \\
//cantUsuarios == cantUsuarios@C6 \ylogico lista == lista@C6 \ylogico dupla == dupla@C6 $
\begin{lstlisting}
}
\end{lstlisting}

\section{Demostraci\'on del cuerpo del problema}
Suponiendo que el ciclo es correcto respecto de su especificaci\'on, queremos ver que vale la poscondici\'on del problema.

\begin{problema}{infoGatewaysTE}{te: TelCO}{[(Gateway,\ent,\ent)]}
  \asegura[infoCorrecta]{mismos(result,\comp{(g,(\longitud{trivias(g)}, cuantosJueganAlgunaTrivia(te,g)))}{g \selec gateways(te)]})}
\end{problema}

$//Qc: Vale\ mismos(lista, \comp{(gateways(this)_j,(\longitud{trivias(gateways(this)_j)},\\
//cuantosJueganAlgunaTrivia(this, gateways(this)_j)))}{j \selec [0..\longitud{gateways(this)})})$
\begin{lstlisting}
  return lista;
}
\end{lstlisting}

Por propiedad de listas podemos afirmar que: \\
$mismos(\comp{(g,(\longitud{trivias(g)}, cuantosJueganAlgunaTrivia(this,g)))}{g \selec gateways(this)]}, \\
\comp{(gateways(this)_j,(\longitud{trivias(gateways(this)_j)}, \\cuantosJueganAlgunaTrivia(this, gateways(this)_j)))}{j \selec [0..\longitud{gateways(this)})}$ \\
simplemente cambiando los selectores de listas por los \'indices correspondientes.

Luego, probamos que el valor del return (la variable lista) cumple la poscondici\'on del problema, es decir, que vale \\
$mismos(lista,\comp{(g,(\longitud{trivias(g)}, cuantosJueganAlgunaTrivia(this,g)))}{g \selec gateways(this)]})$

\section{Demostraci\'on del cuerpo del ciclo}

\subsection{$Pc \implica I$}
Supongamos que vale Pc. Queremos ver que vale I. \\
$Pc: lista == [] \ylogico dupla == (,) \ylogico \\
//i == cantTrivias == cantUsuarios == 0$ \\
$I: 0 \leq i \leq \longitud{gateways(this)} \ylogico \\
mismos (lista, \\
\comp{(gateways(this)_j,(\longitud{trivias(gateways(this)_j)}, cuantosJueganAlgunaTrivia(this, gateways(this)_j)))}{j \selec [0..i)})$ \\
Por Pc sabemos que $ i == 0 \ylogico lista == [] $. Luego, reemplazando en I, queremos ver que: \\
$I: 0 \leq 0 \leq \longitud{gateways(this)} (1) \\
\ylogico mismos([], \\
\comp{(gateways(this)_j,(\longitud{trivias(gateways(this)_j)}, cuantosJueganAlgunaTrivia(this, gateways(this)_j)))}{j \selec [0..0)})  (2) $ \\

Vamos a probar por separado (1) y (2) suponiendo que vale Pc.
(1): Es trivial sabiendo que la longitud de una lista es siempre mayor o igual a 0, y que $ 0 == 0 $ por lo que $ 0 \leq 0 $ \\

(2): Como j va tomando todos los valores en la lista [0..0), que es una lista vac\'ia (propiedad de listas), la lista resultante va a ser tambi\'en vac\'ia. \\
Por lo tanto $mismos ( [], \comp{(gateways(this)_j,(\longitud{trivias(gateways(this)_j)},\\
cuantosJueganAlgunaTrivia(this, gateways(this)_j)))}{j \selec [0..0)}) \implica \\
mismos ( lista, \comp{(gateways(this)_j,(\longitud{trivias(gateways(this)_j)},\\
cuantosJueganAlgunaTrivia(this, gateways(this)_j)))}{j \selec [0..0)})$\\ que es lo que quer\'iamos demostrar.\\


\subsection{La funci\'on variante es estrictamente decreciente}
$Funcion\ variante\ V: \longitud{gateways(this)} - i$
Queremos ver que $ V@C7 < V@C1 $. Sabemos que la longitud de los gateways no se modifica y que $ i@C7 == i@C1 + 1 $ por la transformaci\'on de estados.
Luego, $ V@C1 == \longitud{gateways(this)} - i@C1 > \longitud{gateways(this)} - (i@C1 + 1) == \longitud{gateways(this)} - i@C7 == V@C7 $.

\subsection{$V < 0 \implica \neg B$}
$Funcion\ variante\ V: \longitud{gateways(this)} - i \\
B: i < \longitud{gateways(this)} $ \\
Queremos ver que si $ V < 0 $ el ciclo termina, es decir que vale $ \neg B $. Sabemos que: \\
$ V < 0 \implica \longitud{gateways(this)} - i < 0 \implica i > \longitud{gateways(this)} \implica \neg B $

\subsection{$I \ylogico \neg Telco y que entonces quedan igualB \implica Qc $}
$I: 0 \leq i \leq \longitud{gateways(this)} \ylogico \\
mismos (lista, \\
	\comp{(gateways(this)_j,(\longitud{trivias(gateways(this)_j)}, cuantosJueganAlgunaTrivia(this, gateways(this)_j)))}{j \selec [0..i)}) \\
B: i < \longitud{gateways(this)} $ \\

$\neg B \implica i \geq \longitud{gateways(this)} $ y a su vez $ I \implica 0 \leq i \leq \longitud{gateways(this)} $. Juntando ambos concluimos \\
que $ \longitud{gateway(this)} \leq i \leq \longitud{gateway(this)} \implica i == \longitud{gateway(this)}$. \\

Reemplazando en el resto de I tenemos que:
$mismos (lista, \comp{(gateways(this)_j,(\longitud{trivias(gateways(this)_j)},\\
cuantosJueganAlgunaTrivia(this, gateways(this)_j)))}{j \selec [0..\longitud{gateway(this)})})$ \\
que es exactamente Qc.

\subsection{El cuerpo del ciclo preserva el invariante}
Volvamos a la trasnformaci\'on de estados y sigamos las implicaciones.

\begin{lstlisting}
while (i < gateways().longitud()){
\end{lstlisting}
$//C1: Vale\ I \ylogico B \\
//Implica: 0 \leq i < \longitud{gateways(this)} \ylogico \\
//mismos (lista, \comp{(gateways(this)_j,(\longitud{trivias(gateways(this)_j)}, cuantosJueganAlgunaTrivia(this, gateways(this)_j)))}{j \selec [0..i)})$ \\
\begin{lstlisting}
  Gateway g = gateways().iesimo(i);
\end{lstlisting}
$//C2: Vale\ g == gateways(this)_{i@C1} \ylogico i == i@C1 \ylogico cantTrivias == cantTrivias@C1 \ylogico \\
//cantUsuarios == cantUsuarios@C1 \ylogico lista == lista@C1 \ylogico dupla == dupla@C1 $
\begin{lstlisting}
  cantTrivias = g.trivias().longitud();
\end{lstlisting}
$//C3: Vale\ g == g@C2 \ylogico i == i@C2 \ylogico cantTrivias == \longitud{trivias(g@C2)} \ylogico \\
//cantUsuarios == cantUsuarios@C2 \ylogico lista == lista@C2 \ylogico dupla == dupla@C2 \\
//Implica: g == gateways(this)_{i@C1} \ylogico i == i@C1 \ylogico cantTrivias == \longitud{trivias(g)} \ylogico \\
//lista == lista@C1 \\
//Implica: cantTrivias == \longitud{trivias(gateways(this)_{i@C1})}$
\begin{lstlisting}
  cantUsuarios = usuariosDeLasTrivias (g);
\end{lstlisting}
$//C4: Vale\ g == g@C3 \ylogico i == i@C3 \ylogico cantTrivias == cantTrivias@C3 \ylogico \\
//cantUsuarios == cuantosJueganAlgunaTrivia(this, trivias(g@C3)) \ylogico lista == lista@C3 \ylogico dupla == dupla@C3 \\ $
$//Implica: g == gateways(this)_{i@C1} \ylogico i == i@C1 \ylogico cantTrivias == \longitud{trivias(gateways(this)_{i@C1})} \ylogico \\
//cantUsuarios == cuantosJueganAlgunaTrivia(this, trivias(g@C1)) \ylogico lista == lista@C1 $
Ac\'a usamos la poscondici\'on de usuariosDeLasTrivias, sabiendo que los par\'ametros cumplen la precondici\'ion.
\begin{lstlisting}
  dupla.first = g;
  dupla.second = pair <int,int> (cantTrivias,cantUsuarios);
\end{lstlisting}
$//C5: Vale\ g == g@C4 \ylogico i == i@C4 \ylogico cantTrivias == cantTrivias@C4 \ylogico \\
//cantUsuarios == cantUsuarios@C4 \ylogico lista == lista@C4 \ylogico \\
//dupla == (g@C4,(cantTrivias@C4,cantUsuarios@C4)) \\
//Implica: i == i@C1 \ylogico lista == lista@C1 \\
//\ylogico dupla == (gateways(this)_{i@C1},(\longitud{trivias(gateways(this)_{i@C1})},cuantosJueganAlgunaTrivia(this, trivias(g@C1))))$
\begin{lstlisting}
  lista.agregar(dupla);
\end{lstlisting}
$//C6: Vale\ g == g@C5 \ylogico i == i@C5 \ylogico cantTrivias == cantTrivias@C5 \ylogico \\
//cantUsuarios == cantUsuarios@C5 \ylogico lista == dupla@C5 : lista@C5 \ylogico dupla == dupla@C5 \\
//Implica: i == i@C1 \ylogico mismos (lista, (gateways(this)_{i@C1},(\longitud{trivias(gateways(this)_{i@C1})}, \\
//cuantosJueganAlgunaTrivia(tTelco y que entonces quedan igualhis, trivias(g@C1)))) : lista@C1)$
\begin{lstlisting}
  i++;
\end{lstlisting}(de hecho tampoco los usamos) 
$//C7: Vale\ g == g@C6 \ylogico i == i@C6 + 1 \ylogico cantTrivias == cantTrivias@C6 \ylogico \\
//cantUsuarios == cantUsuarios@C6 \ylogico lista == lista@C6 \ylogico dupla == dupla@C6 \\
//Implica: i == i@C1 + 1 \ylogico mismos (lista, (gateways(this)_{i@C1},(\longitud{trivias(gateways(this)_{i@C1})}, \\
//cuantosJueganAlgunaTrivia(this, trivias(g@C1)))) : lista@C1)$
\begin{lstlisting}
}
\end{lstlisting}


Queremos probar que el invariante vale en C7 suponiendo que val\'ia en C1, y usando las implicaciones de la transformaci\'on de estados.
$I: 0 \leq i \leq \longitud{gateways(this)} (1) \ylogico \\
mismos(lista, \comp{(gateways(this)_j,(\longitud{trivias(gateways(this)_j)},\\
cuantosJueganAlgunaTrivia(this, gateways(this)_j)))}{j \selec [0..i)})$ (2) \\

Probaremos por separado (1) y (2). \\
(1): Sabemos que $i@C7 == i@C1 + 1$. Como para entrar al ciclo hac\'ia falta que valiera B, eso quiere decir que $i@C1 < \longitud{gateways(this)}$.
Como tanto $i$ como $\longitud{gateways(this)}$ son enteras, podemos concluir que en C7 $i \leq \longitud{gateways(this)}$.
Como el invariante val\'ia en C1, sabemos tambi\'en que $0 \leq i@C1 \implica 0 \leq i@1 + 1$.
\\
(2): En C6, tenemos que \\
$i == i@C1 \ylogico \\
mismos (lista, (gateways(this)_{i@C1},(\longitud{trivias(gateways(this)_{i@C1})},cuantosJueganAlgunaTrivia(this, trivias(g@C1)))) \\
: lista@C1)$ \\
Como el invariante val\'ia en C1, esto implica que \\
$mismos (lista, (gateways(this)_{i@C1},(\longitud{trivias(gateways(this)_{i@C1})},cuantosJueganAlgunaTrivia(this, trivias(g@C1)))) \\
: \comp{(gateways(this)_j,(\longitud{trivias(gateways(this)_j)}, cuantosJueganAlgunaTrivia(this, gateways(this)_j)))}{j \selec [0..i)})$ \\
\\
Podemos ver que el nuevo elemento tiene la forma de la expresi\'on de la lista por compresi\'on para $j == i$. Entonces, \\
sabiendo que los gateways no fueron modificados (ver aclaraci\'on al inicio) podemos comprimir la lista en esta nueva expresi\'on: \\
$mismos (lista, \\
	 \comp{(gateways(this)_j,(\longitud{trivias(gateways(this)_j)},cuantosJueganAlgunaTrivia(this, gateways(this)_j)))}{j \selec [0..i]})$ \\
En C7, $i == i@C6 + 1$, por lo tanto la lista quedar\'ia: \\
$mismos (lista, \\
	\comp{(gateways(this)_j,(\longitud{trivias(gateways(this)_j)},cuantosJueganAlgunaTrivia(this, gateways(this)_j)))}{j \selec [0..i)})$ \\
por propiedad de listas ($[0..i] == [0..i+1)$). Y esta expresi\'on es exactamente (2). $\square$

\medskip

Queda probado el teorema del invariante para el cuerpo del ciclo principal. Falta demostrar la correctitud de las funciones auxiliares.
